Left Termination of the query pattern
f_in_1(g)
w.r.t. the given Prolog program could successfully be proven:
↳ Prolog
↳ PrologToPiTRSProof
Clauses:
f(X) :- g(s(s(s(X)))).
f(s(X)) :- f(X).
g(s(s(s(s(X))))) :- f(X).
Queries:
f(g).
We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
f_in(s(X)) → U2(X, f_in(X))
f_in(X) → U1(X, g_in(s(s(s(X)))))
g_in(s(s(s(s(X))))) → U3(X, f_in(X))
U3(X, f_out(X)) → g_out(s(s(s(s(X)))))
U1(X, g_out(s(s(s(X))))) → f_out(X)
U2(X, f_out(X)) → f_out(s(X))
The argument filtering Pi contains the following mapping:
f_in(x1) = f_in(x1)
s(x1) = s(x1)
U2(x1, x2) = U2(x2)
U1(x1, x2) = U1(x2)
g_in(x1) = g_in(x1)
U3(x1, x2) = U3(x2)
f_out(x1) = f_out
g_out(x1) = g_out
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
Pi-finite rewrite system:
The TRS R consists of the following rules:
f_in(s(X)) → U2(X, f_in(X))
f_in(X) → U1(X, g_in(s(s(s(X)))))
g_in(s(s(s(s(X))))) → U3(X, f_in(X))
U3(X, f_out(X)) → g_out(s(s(s(s(X)))))
U1(X, g_out(s(s(s(X))))) → f_out(X)
U2(X, f_out(X)) → f_out(s(X))
The argument filtering Pi contains the following mapping:
f_in(x1) = f_in(x1)
s(x1) = s(x1)
U2(x1, x2) = U2(x2)
U1(x1, x2) = U1(x2)
g_in(x1) = g_in(x1)
U3(x1, x2) = U3(x2)
f_out(x1) = f_out
g_out(x1) = g_out
Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
F_IN(s(X)) → U21(X, f_in(X))
F_IN(s(X)) → F_IN(X)
F_IN(X) → U11(X, g_in(s(s(s(X)))))
F_IN(X) → G_IN(s(s(s(X))))
G_IN(s(s(s(s(X))))) → U31(X, f_in(X))
G_IN(s(s(s(s(X))))) → F_IN(X)
The TRS R consists of the following rules:
f_in(s(X)) → U2(X, f_in(X))
f_in(X) → U1(X, g_in(s(s(s(X)))))
g_in(s(s(s(s(X))))) → U3(X, f_in(X))
U3(X, f_out(X)) → g_out(s(s(s(s(X)))))
U1(X, g_out(s(s(s(X))))) → f_out(X)
U2(X, f_out(X)) → f_out(s(X))
The argument filtering Pi contains the following mapping:
f_in(x1) = f_in(x1)
s(x1) = s(x1)
U2(x1, x2) = U2(x2)
U1(x1, x2) = U1(x2)
g_in(x1) = g_in(x1)
U3(x1, x2) = U3(x2)
f_out(x1) = f_out
g_out(x1) = g_out
G_IN(x1) = G_IN(x1)
U11(x1, x2) = U11(x2)
U31(x1, x2) = U31(x2)
U21(x1, x2) = U21(x2)
F_IN(x1) = F_IN(x1)
We have to consider all (P,R,Pi)-chains
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
Pi DP problem:
The TRS P consists of the following rules:
F_IN(s(X)) → U21(X, f_in(X))
F_IN(s(X)) → F_IN(X)
F_IN(X) → U11(X, g_in(s(s(s(X)))))
F_IN(X) → G_IN(s(s(s(X))))
G_IN(s(s(s(s(X))))) → U31(X, f_in(X))
G_IN(s(s(s(s(X))))) → F_IN(X)
The TRS R consists of the following rules:
f_in(s(X)) → U2(X, f_in(X))
f_in(X) → U1(X, g_in(s(s(s(X)))))
g_in(s(s(s(s(X))))) → U3(X, f_in(X))
U3(X, f_out(X)) → g_out(s(s(s(s(X)))))
U1(X, g_out(s(s(s(X))))) → f_out(X)
U2(X, f_out(X)) → f_out(s(X))
The argument filtering Pi contains the following mapping:
f_in(x1) = f_in(x1)
s(x1) = s(x1)
U2(x1, x2) = U2(x2)
U1(x1, x2) = U1(x2)
g_in(x1) = g_in(x1)
U3(x1, x2) = U3(x2)
f_out(x1) = f_out
g_out(x1) = g_out
G_IN(x1) = G_IN(x1)
U11(x1, x2) = U11(x2)
U31(x1, x2) = U31(x2)
U21(x1, x2) = U21(x2)
F_IN(x1) = F_IN(x1)
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 3 less nodes.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
Pi DP problem:
The TRS P consists of the following rules:
F_IN(X) → G_IN(s(s(s(X))))
F_IN(s(X)) → F_IN(X)
G_IN(s(s(s(s(X))))) → F_IN(X)
The TRS R consists of the following rules:
f_in(s(X)) → U2(X, f_in(X))
f_in(X) → U1(X, g_in(s(s(s(X)))))
g_in(s(s(s(s(X))))) → U3(X, f_in(X))
U3(X, f_out(X)) → g_out(s(s(s(s(X)))))
U1(X, g_out(s(s(s(X))))) → f_out(X)
U2(X, f_out(X)) → f_out(s(X))
The argument filtering Pi contains the following mapping:
f_in(x1) = f_in(x1)
s(x1) = s(x1)
U2(x1, x2) = U2(x2)
U1(x1, x2) = U1(x2)
g_in(x1) = g_in(x1)
U3(x1, x2) = U3(x2)
f_out(x1) = f_out
g_out(x1) = g_out
G_IN(x1) = G_IN(x1)
F_IN(x1) = F_IN(x1)
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
Pi DP problem:
The TRS P consists of the following rules:
F_IN(X) → G_IN(s(s(s(X))))
F_IN(s(X)) → F_IN(X)
G_IN(s(s(s(s(X))))) → F_IN(X)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RFCMatchBoundsDPProof
Q DP problem:
The TRS P consists of the following rules:
F_IN(X) → G_IN(s(s(s(X))))
F_IN(s(X)) → F_IN(X)
G_IN(s(s(s(s(X))))) → F_IN(X)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
Termination of the TRS P cup R can be shown by a matchbound [6,7] of 2. This implies finiteness of the given DP problem.
The following rules (P cup R) were used to construct the certificate:
F_IN(X) → G_IN(s(s(s(X))))
F_IN(s(X)) → F_IN(X)
G_IN(s(s(s(s(X))))) → F_IN(X)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
54, 55, 58, 57, 56, 59, 61, 60, 62, 64, 63
Node 54 is start node and node 55 is final node.
Those nodes are connect through the following edges:
- 54 to 56 labelled G_IN_1(0)
- 54 to 55 labelled F_IN_1(0), F_IN_1(1)
- 54 to 59 labelled G_IN_1(1)
- 54 to 62 labelled G_IN_1(2)
- 55 to 55 labelled #_1(0)
- 58 to 55 labelled s_1(0)
- 57 to 58 labelled s_1(0)
- 56 to 57 labelled s_1(0)
- 59 to 60 labelled s_1(1)
- 61 to 55 labelled s_1(1)
- 60 to 61 labelled s_1(1)
- 62 to 63 labelled s_1(2)
- 64 to 55 labelled s_1(2)
- 63 to 64 labelled s_1(2)